| Definitions | SQType(T), {T}, e c e',  x:A. B(x), P  Q,  e@i. P(e), Knd, weak-precond-send-p(es;T;A;l;tg;a;ds;P;f), A c B, sframe-p-realizable, usends1-p-realizable, Normal(T), Rplus-right(x1), Rplus-left(x1), if b then t else f fi , tt, ff, Rplus?(x1),  b, True, Y, reduce(f;k;as),  (L), pre-p-realizable, es-realizer(p), t.2, t.1, P & Q, at src(l):action $a(m) precondition P sends [$tg,f] on link l, suptype(S; T), S  T,   x. t(x),  , t  T, "$x", P   Q, Id, x:A. B(x), Trans(T;x,y.E(x;y)), Dec(P), e' e.P(e'), P  Q, only events in L send on l with tg, usends1-p(es;ds;k;T;l;tg;B;f), @i Precondition for a:Outcome(p) is P:State(ds)   , Unit, False, R ||- es.P(es),  es.P(es), Realizer, x(s), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Reffect(loc;ds;knd;T;x;f), Rframe(loc;T;x;L), Rinit(loc;T;x;v),  , Rnone(), left right, Rsframe(lnk;tag;L), Rsends(ds;knd;T;l;dt;g), Rpre(loc;ds;a;p;P), x {FDLNOr12445} |